Require Export Matrix.Mat.Matrix_Module.
Require Export Matrix.MMat.MMatrix_Module.
Require Extraction.
Require Export Reals.

Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

Section MM.
Variable A:Set.
Variable m n :nat.
Definition mmatrix_each f:=@matrix_each (Mat A m n) (@matrix_each A f m n).
Definition mmatrix_map f:= @matrix_map (Mat A m n) (@matrix_map A f m n).
End MM.

Extraction "matrix.ml" matrix_map matrix_each matrix_mul trans
  mmatrix_each mmatrix_map mmtrans mmatrix_mul MM_to_M.
